Inference at * 
Iof proof for Lemma inconsistent-bool-eq:


  (tt = ff)  False 

latex

 by Auto 

latex

 1: 

 1: 1. tt = ff
 1:   False
 .

Definitions	P  Q, P & Q, P  Q, P  Q, Void, , s = t, , tt, ff, t  T, False
Lemmas	bool wf, btrue wf, bfalse wf, false wf